package karpiel.boguchwal.wojciech.przemek

import karpiel.boguchwal.wojciech.przemek.Ast._
import karpiel.boguchwal.wojciech.przemek.Cache.InnerCache

object TypeNormalizer {

  /**
    * multi-pass normalization
    * To jest ciężkie ale konieczne
    */
  def normalized(expr: Ast)(implicit ctx: Context, cache: Cache): Ast = {
    implicit val cc: Cache.InnerCache = cache.getFor(ctx)
    cc.normalize(expr, {
    val afterSinglePass = singlePassNormalization(expr)
    if (afterSinglePass == expr) afterSinglePass
    else normalized(afterSinglePass)
    })
  }

  //TODO zoptymalizować bo dużo rzeczy w środku pojedynczego przebiegu przechodzi na wielobieg
  private def singlePassNormalization(expr: Ast)(implicit ctx: Context, cache: Cache, cc: InnerCache): Ast = {
    expr match {
      case b: Bruijn => ctx.getValue(b).map(_.normalizeCC).getOrElse(b)
      case PiType(typeT, value) => PiType(typeT.normalizeCC, value.normalized(ctx.append(typeT), implicitly))
      case PiValue(typeT, value) => PiValue(typeT.normalizeCC, value.normalized(ctx.append(typeT), implicitly))
      //todo jakoś normalniej to zrobić dla J\
      case PiElim(PiElim(PiElim(J(typeFunc, reflFunc), x), y), id) =>
        if (jElimCheck(x, y, id, cc)) { //I want to avoid guards in pattern matching when rewriting with futures
          J(typeFunc, reflFunc).inferType
          reflFunc.getAs[PiValue].typeT.assertEqualsOpt(x.inferType)
          PiElim(reflFunc, x).normalizeCC
        }else{
          PiElim(PiElim(PiElim(J(typeFunc, reflFunc), x), y).normalizeCC, id.normalizeCC)
        }
      case PiElim(piValue, argument) =>
        val normalizedArg = argument.normalizeCC
        piValue.normalizeCC match {
          case PiValue(typeT, value) =>
            typeT.assertEqualsOpt(normalizedArg.inferType) //typecheck
            Utils.unshift(value.normalized(ctx.append(typeT, normalizedArg), implicitly), 0, 1)
          case SumElim(aFn, bFn) =>
            argument.normalizeCC match {
              case SumInl(aValue, bType) =>
                bFn.normalizeCC match { //typecheck
                  case PiValue(typeT, _) => typeT.assertEqualsOpt(bType)
                  case _ =>
                }
                PiElim(aFn, aValue).normalizeCC //aFn will be checked by PiElim
              case SumInr(aType, bValue) =>
                aFn.normalizeCC match { //typecheck
                  case PiValue(typeT, _) => typeT.assertEqualsOpt(aType)
                  case _ =>
                }
                PiElim(bFn, bValue).normalizeCC //bFn will be checked by PiElim
              case any => PiElim(any, normalizedArg) //todo a może illegal?
            }
          case BoolElim(ifTrue, ifFalse) =>
            BoolElim(ifTrue, ifFalse).inferType //check
            normalizedArg match {
              case BoolTrue => ifTrue.normalizeCC
              case BoolFalse => ifFalse.normalizeCC
              case other => PiElim(BoolElim(ifTrue.normalizeCC, ifFalse.normalizeCC), normalizedArg)
            }
          case BoolRec(boolToType, ifTrue, ifFalse) =>
            TypeInferer.inferTypeNoNorm(BoolRec(boolToType.normalizeCC, ifTrue.normalizeCC, ifFalse.normalizeCC)) //check
            normalizedArg match {
              case BoolTrue => ifTrue
              case BoolFalse => ifFalse
              case todo => PiElim(BoolRec(boolToType.normalizeCC, ifTrue.normalizeCC, ifFalse.normalizeCC), normalizedArg)
            }
          case elim@SigmaElim(PiValue(xType, PiValue(aXType, ex))) =>
            normalizedArg match {
              case s@SigmaValue(x, aX, a) =>
                if (a.normalized(ctx.append(x.inferType, x), implicitly) != aX.inferType)
                  throw new TypecheckException(a.normalized(ctx.append(x.inferType, x), implicitly) + " != " + aX)
                x.inferType.assertEqualsOpt(xType)
                val axTypeNorm = aXType.normalized(ctx.append(xType, x), implicitly)
                if (aX.inferType.normalizeCC != axTypeNorm)
                  throw new TypecheckException()
                PiElim(PiElim(PiValue(xType, PiValue(aXType, ex)), x), aX).normalizeCC
              case any => PiElim(elim, normalizedArg)
            }
          case w@WElim(e, fn) if normalizedArg.inferType.normalizeCC.isInstanceOf[WType] =>
            val pi = w.inferType.getAs[PiType]
            normalizedArg match {
              case sup: Ast.WSup => //xD
                PiElim(PiElim(PiElim(fn, sup.label), sup.fn), PiValue(sup.fn.inferType.getAs[PiType].typeT, PiElim(w, PiElim(sup.fn, Bruijn(0))))).normalizeCC
              case anyElseArgType => PiElim(w, anyElseArgType)
            }
          case anyElse => PiElim(anyElse, normalizedArg)
        }
      case s@SigmaValue(x, aX, aType) =>
        //copied form infeerre
        val xType = x.inferType.normalizeCC
        if (aType.normalized(ctx.append(xType, x), implicitly) != aX.inferType.normalizeCC)
          throw new TypecheckException() //no assertEquals because context mismatch

        SigmaValue(x.normalizeCC, aX.normalizeCC, aType /* BEZ NORMALIZACJI bo tracimy informacje .normalized(ctx.append(x.inferType,x))*/)
      case Proj1(q) =>
        q.normalizeCC match {
          case s: SigmaValue => s.x
          case e => Proj1(e)
        }
      case Proj2(q) =>
        q.normalizeCC match {
          case s: SigmaValue => s.aX
          case e => Proj2(e)
        }
      case WSup(wType_, label_, fn_) if wType_.normalizeCC.isInstanceOf[WType] => //czy to ma jakiś sens vs applyToSubtrees?
        val wType = wType_.getAs[WType]
        val label = label_.normalizeCC
        val fn = fn_.normalizeCC
        //typecheck!
        TypeInferer.inferTypeNoNorm(WSup(wType, label, fn))
        wType.arityFn.getAs[PiType] //todo tu nie lbl
        WSup(wType, label, fn)
      case we@WElim(e, eSup) => //todo może dodać inferNoNorm to applyToSubtrees?
        TypeInferer.inferTypeNoNorm(WElim(e.normalizeCC, eSup.normalizeCC))
        WElim(e.normalizeCC, eSup.normalizeCC)
      case _: NamedType => throw new TypecheckException()
      case _: Var => throw new TypecheckException()
      case any => Utils.applyToSubTrees(any, { q =>
        q.inferType //todo turbo niewydajne ale łapie błędy
      val w = q.normalizeCC
        //        w.inferType
        w
      })
    }
  }

  private def jElimCheck(x: Ast, y: Ast, id: Ast, commonCache: InnerCache)(implicit ctx: Context, cache: Cache) = {
    implicit val cc = commonCache
    x.equalNormalized(y) && id.equalNormalized(Refl(x))
  }
}
